qrng  crng{i:l} 

latex

Definitions

x. t(x), rng_eq(r), eqfun_p(T; eq), True, T, bilinear(T; pl; tm), P  Q, P  Q, ident(T; op; id), assoc(T; op), monoid_p(T; op; id), igrp{i:l}, imon{i:l}, group_p(T; op; id; inv), rng_one(r), rng_minus(r), rng_zero(r), rng_plus(r), ring_p(T; plus; zero; neg; times; one), prop{i:l}, ff, tt, P  Q, if b then t else f fi , rng_sig{i:l}, P  Q, rng{i:l}, t.2, t.1, x f y, x:A. B(x), rng_times(r), rng_car(r), comm(T; op), qrng, crng{i:l}, t  T, x(s), grp_inv(g), mon{i:l}, abmonoid{i:l}, ocmon{i:l}, ocgrp{i:l}, qadd_grp, grp_id(g), grp_op(g), grp_car(g), Unit, , subtype(S; T),

Lemmas

iff functionality wrt iff, iff wf, all functionality wrt iff, q distrib, true wf, squash wf, qmul ident, qmul assoc, grp inv wf, inverse wf, igrp properties, ocgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf2, imon properties, unit wf, qdiv wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, it wf, assert-qeq, eqtt to assert, assert wf, iff transitivity, bool wf, qmul wf, int inc rationals, qadd wf, q le wf, qeq wf2, rng eq wf, eqfun p wf, rng one wf, rng minus wf, rng zero wf, rng plus wf, ring p wf, rng times wf, rng car wf, comm wf, rationals wf, qmul com